﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using TruthTree2.FOL.Logic;
using TruthTree2.FOL.ResolutionExtensions;

namespace TruthTree2.FOL.Resolution
{
    public class Set
    {
        internal List<Clause> clauses;

        public Set(params Clause[] c)
        {
            clauses = new List<Clause>(c);
        }

        public Set(List<Clause> c)
        {
            clauses = c;
        }

        public Set Union(Set s)
        {
            List<Clause> cl = new List<Clause>();
            cl.AddRange(clauses);

            foreach (Clause c in s.clauses)
            {
                if (!cl.Contains(c)) { cl.Add(c); }
            }

            return new Set(cl);
        }

        public bool Resolution()
        {
            /* 1. Find two clauses containing the same predicate, where it is negated in
                  one clause but not in the other.
               2. Perform a unification on the two predicates. (If the unification fails,
                  you made a bad choice of predicates. Go back to the previous step and try again.)
               3. If any unbound variables which were bound in the unified predicates also
                  occur in other predicates in the two clauses, replace them with their bound
                  values (terms) there as well.
               4. Discard the unified predicates, and combine the remaining ones from the
                  two clauses into a new clause, also joined by the "∨" operator.
             */

            List<Clause> local = new List<Clause>(clauses);
            do
            {
                //local.Sort((a, b) => { return a.arity.CompareTo(b.arity); });
                List<Clause> newresolvents = new List<Clause>();
                bool subset = false;
                for (int a = 0; a < local.Count; a++)
                {
                    for (int b = 0; b < local.Count; b++)
                    {
                        if (a == b) { continue; }

                        Clause res;
                        if (local[a].Unify(local[b], out res))
                        {
                            if (res.arity == 0) { return true; }
                            if (!local.Contains(res))
                            {
                                newresolvents.Add(res);
                                subset = true;
                            }
                        }
                    }
                }

                if (!subset) { return false; }

                local.AddRange(newresolvents);
            } while (true);
        }

        private void printlist<T>(List<T> items)
        {
            foreach (T i in items)
            {
                Console.WriteLine("{0}", i);
            }
        }

        public override string ToString()
        {
            return String.Join(", ", clauses);
        }

        private static Clause clausifyWFF(WFF f)
        {
            if (f is Disjunction)
            {
                Disjunction d = (Disjunction)f;
                List<Literal> literals = new List<Literal>();
                foreach (WFF a in d.disjuncts)
                {
                    if (a is Negation)
                    {
                        Negation n = (Negation)a;
                        literals.Add(new Literal((AtomicWFF)n.inner, true));
                    }
                    else if (a is AtomicWFF)
                    {
                        literals.Add(new Literal((AtomicWFF)a, false));
                    }
                }

                return new Clause(literals.ToArray());
            }
            else if (f is Negation)
            {
                Negation n = (Negation)f;
                return new Clause(new Literal((AtomicWFF)n.inner, true));
            }
            else if (f is AtomicWFF)
            {
                return new Clause(new Literal((AtomicWFF)f, false));
            }

            throw new NotImplementedException(f.GetType().ToString());
        }

        private static Set wffToSet(WFF f)
        {
            if (f is Conjunction)
            {
                Conjunction c = (Conjunction)f;
                List<Clause> clauses = new List<Clause>();
                foreach (WFF a in c.conjuncts)
                {
                    clauses.Add(clausifyWFF(a));
                }

                return new Set(clauses);
            }
            else if (f is Disjunction || f is Negation || f is AtomicWFF)
            {
                return new Set(clausifyWFF(f));
            }

            throw new NotImplementedException(f.GetType().ToString());
        }

        public static Set ToResolutionSet(WFF f)
        {
            WFF cnf = f.ConvertToCNF();

            return wffToSet(cnf);
        }
        
    }
}
